type Color_Type is (Red, Green, Blue);

procedure Exchange (X, Y: in out Color_Type);
--# derives X from Y &
--#         Y from X;
--# post X = Y~ and Y = X~;
